The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

walk#1(Leaf(x2)) → cons_x(x2)
walk#1(Node(x5, x3)) → comp_f_g(walk#1(x5), walk#1(x3))
comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) → comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
comp_f_g#1(comp_f_g(x7, x9), cons_x(x2), x4) → comp_f_g#1(x7, x9, Cons(x2, x4))
comp_f_g#1(cons_x(x2), comp_f_g(x5, x7), x3) → Cons(x2, comp_f_g#1(x5, x7, x3))
comp_f_g#1(cons_x(x5), cons_x(x2), x4) → Cons(x5, Cons(x2, x4))
main(Leaf(x4)) → Cons(x4, Nil)
main(Node(x9, x5)) → comp_f_g#1(walk#1(x9), walk#1(x5), Nil)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

walk#1(Leaf(x2)) → cons_x(x2) [1]
walk#1(Node(x5, x3)) → comp_f_g(walk#1(x5), walk#1(x3)) [1]
comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) → comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) [1]
comp_f_g#1(comp_f_g(x7, x9), cons_x(x2), x4) → comp_f_g#1(x7, x9, Cons(x2, x4)) [1]
comp_f_g#1(cons_x(x2), comp_f_g(x5, x7), x3) → Cons(x2, comp_f_g#1(x5, x7, x3)) [1]
comp_f_g#1(cons_x(x5), cons_x(x2), x4) → Cons(x5, Cons(x2, x4)) [1]
main(Leaf(x4)) → Cons(x4, Nil) [1]
main(Node(x9, x5)) → comp_f_g#1(walk#1(x9), walk#1(x5), Nil) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

walk#1(Leaf(x2)) → cons_x(x2) [1]
walk#1(Node(x5, x3)) → comp_f_g(walk#1(x5), walk#1(x3)) [1]
comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) → comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) [1]
comp_f_g#1(comp_f_g(x7, x9), cons_x(x2), x4) → comp_f_g#1(x7, x9, Cons(x2, x4)) [1]
comp_f_g#1(cons_x(x2), comp_f_g(x5, x7), x3) → Cons(x2, comp_f_g#1(x5, x7, x3)) [1]
comp_f_g#1(cons_x(x5), cons_x(x2), x4) → Cons(x5, Cons(x2, x4)) [1]
main(Leaf(x4)) → Cons(x4, Nil) [1]
main(Node(x9, x5)) → comp_f_g#1(walk#1(x9), walk#1(x5), Nil) [1]

The TRS has the following type information:

walk#1 :: Leaf:Node → cons_x:comp_f_g Leaf :: a → Leaf:Node cons_x :: a → cons_x:comp_f_g Node :: Leaf:Node → Leaf:Node → Leaf:Node comp_f_g :: cons_x:comp_f_g → cons_x:comp_f_g → cons_x:comp_f_g comp_f_g#1 :: cons_x:comp_f_g → cons_x:comp_f_g → Cons:Nil → Cons:Nil Cons :: a → Cons:Nil → Cons:Nil main :: Leaf:Node → Cons:Nil Nil :: Cons:Nil

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

walk#1(v0) → null_walk#1 [0]
comp_f_g#1(v0, v1, v2) → null_comp_f_g#1 [0]
main(v0) → null_main [0]

And the following fresh constants:

null_walk#1, null_comp_f_g#1, null_main, const, const1

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: walk#1(Leaf(x2)) → cons_x(x2) [1] walk#1(Node(x5, x3)) → comp_f_g(walk#1(x5), walk#1(x3)) [1] comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) → comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) [1] comp_f_g#1(comp_f_g(x7, x9), cons_x(x2), x4) → comp_f_g#1(x7, x9, Cons(x2, x4)) [1] comp_f_g#1(cons_x(x2), comp_f_g(x5, x7), x3) → Cons(x2, comp_f_g#1(x5, x7, x3)) [1] comp_f_g#1(cons_x(x5), cons_x(x2), x4) → Cons(x5, Cons(x2, x4)) [1] main(Leaf(x4)) → Cons(x4, Nil) [1] main(Node(x9, x5)) → comp_f_g#1(walk#1(x9), walk#1(x5), Nil) [1] walk#1(v0) → null_walk#1 [0] comp_f_g#1(v0, v1, v2) → null_comp_f_g#1 [0] main(v0) → null_main [0] The TRS has the following type information: walk#1 :: Leaf:Node → cons_x:comp_f_g:null_walk#1 Leaf :: a → Leaf:Node cons_x :: a → cons_x:comp_f_g:null_walk#1 Node :: Leaf:Node → Leaf:Node → Leaf:Node comp_f_g :: cons_x:comp_f_g:null_walk#1 → cons_x:comp_f_g:null_walk#1 → cons_x:comp_f_g:null_walk#1 comp_f_g#1 :: cons_x:comp_f_g:null_walk#1 → cons_x:comp_f_g:null_walk#1 → Cons:Nil:null_comp_f_g#1:null_main → Cons:Nil:null_comp_f_g#1:null_main Cons :: a → Cons:Nil:null_comp_f_g#1:null_main → Cons:Nil:null_comp_f_g#1:null_main main :: Leaf:Node → Cons:Nil:null_comp_f_g#1:null_main Nil :: Cons:Nil:null_comp_f_g#1:null_main null_walk#1 :: cons_x:comp_f_g:null_walk#1 null_comp_f_g#1 :: Cons:Nil:null_comp_f_g#1:null_main null_main :: Cons:Nil:null_comp_f_g#1:null_main const :: Leaf:Node const1 :: a Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

Nil => 0
null_walk#1 => 0
null_comp_f_g#1 => 0
null_main => 0
const => 0
const1 => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 }→ comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) :|: z'' = x1, z' = 1 + x2 + x3, x4 >= 0, x5 >= 0, x1 >= 0, z = 1 + x4 + x5, x2 >= 0, x3 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ comp_f_g#1(x7, x9, 1 + x2 + x4) :|: x4 >= 0, z' = 1 + x2, z = 1 + x7 + x9, z'' = x4, x7 >= 0, x9 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ 1 + x2 + comp_f_g#1(x5, x7, x3) :|: x5 >= 0, x7 >= 0, z = 1 + x2, z'' = x3, x2 >= 0, x3 >= 0, z' = 1 + x5 + x7
comp_f_g#1(z, z', z'') -{ 1 }→ 1 + x5 + (1 + x2 + x4) :|: x5 >= 0, x4 >= 0, z' = 1 + x2, z = 1 + x5, z'' = x4, x2 >= 0
main(z) -{ 1 }→ comp_f_g#1(walk#1(x9), walk#1(x5), 0) :|: x5 >= 0, z = 1 + x9 + x5, x9 >= 0
main(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
main(z) -{ 1 }→ 1 + x4 + 0 :|: x4 >= 0, z = 1 + x4
walk#1(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
walk#1(z) -{ 1 }→ 1 + x2 :|: z = 1 + x2, x2 >= 0
walk#1(z) -{ 1 }→ 1 + walk#1(x5) + walk#1(x3) :|: x5 >= 0, z = 1 + x5 + x3, x3 >= 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V4, V5),0,[fun(V, Out)],[V >= 0]). eq(start(V, V4, V5),0,[fun1(V, V4, V5, Out)],[V >= 0,V4 >= 0,V5 >= 0]). eq(start(V, V4, V5),0,[main(V, Out)],[V >= 0]). eq(fun(V, Out),1,[],[Out = 1 + V1,V = 1 + V1,V1 >= 0]). eq(fun(V, Out),1,[fun(V2, Ret01),fun(V3, Ret1)],[Out = 1 + Ret01 + Ret1,V2 >= 0,V = 1 + V2 + V3,V3 >= 0]). eq(fun1(V, V4, V5, Out),1,[fun1(V8, V9, V10, Ret2),fun1(V6, V7, Ret2, Ret)],[Out = Ret,V5 = V10,V4 = 1 + V8 + V9,V6 >= 0,V7 >= 0,V10 >= 0,V = 1 + V6 + V7,V8 >= 0,V9 >= 0]). eq(fun1(V, V4, V5, Out),1,[fun1(V11, V12, 1 + V13 + V14, Ret3)],[Out = Ret3,V14 >= 0,V4 = 1 + V13,V = 1 + V11 + V12,V5 = V14,V11 >= 0,V12 >= 0,V13 >= 0]). eq(fun1(V, V4, V5, Out),1,[fun1(V16, V17, V18, Ret11)],[Out = 1 + Ret11 + V15,V16 >= 0,V17 >= 0,V = 1 + V15,V5 = V18,V15 >= 0,V18 >= 0,V4 = 1 + V16 + V17]). eq(fun1(V, V4, V5, Out),1,[],[Out = 2 + V19 + V20 + V21,V19 >= 0,V21 >= 0,V4 = 1 + V20,V = 1 + V19,V5 = V21,V20 >= 0]). eq(main(V, Out),1,[],[Out = 1 + V22,V22 >= 0,V = 1 + V22]). eq(main(V, Out),1,[fun(V23, Ret0),fun(V24, Ret12),fun1(Ret0, Ret12, 0, Ret4)],[Out = Ret4,V24 >= 0,V = 1 + V23 + V24,V23 >= 0]). eq(fun(V, Out),0,[],[Out = 0,V25 >= 0,V = V25]). eq(fun1(V, V4, V5, Out),0,[],[Out = 0,V26 >= 0,V5 = V27,V28 >= 0,V = V26,V4 = V28,V27 >= 0]). eq(main(V, Out),0,[],[Out = 0,V29 >= 0,V = V29]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,V4,V5,Out),[V,V4,V5],[Out]). input_output_vars(main(V,Out),[V],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive [multiple] : [fun/2]
1. recursive [multiple] : [fun1/4]
2. non_recursive : [main/2]
3. non_recursive : [start/3]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into fun1/4
2. SCC is partially evaluated into main/2
3. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun/2
* CE 5 is refined into CE [16]
* CE 7 is refined into CE [17]
* CE 6 is refined into CE [18]


### Cost equations --> "Loop" of fun/2
* CEs [18] --> Loop 12
* CEs [16] --> Loop 13
* CEs [17] --> Loop 14

### Ranking functions of CR fun(V,Out)
* RF of phase [12]: [V]

#### Partial ranking functions of CR fun(V,Out)
* Partial RF of phase [12]:
- RF of loop [12:1,12:2]:
V


### Specialization of cost equations fun1/4
* CE 11 is refined into CE [19]
* CE 12 is refined into CE [20]
* CE 9 is refined into CE [21]
* CE 10 is refined into CE [22]
* CE 8 is refined into CE [23]


### Cost equations --> "Loop" of fun1/4
* CEs [23] --> Loop 15
* CEs [21] --> Loop 16
* CEs [22] --> Loop 17
* CEs [19] --> Loop 18
* CEs [20] --> Loop 19

### Ranking functions of CR fun1(V,V4,V5,Out)
* RF of phase [15,16,17]: [V/2+V4/2-1/2]

#### Partial ranking functions of CR fun1(V,V4,V5,Out)
* Partial RF of phase [15,16,17]:
- RF of loop [15:1,15:2,16:1,17:1]:
V/2+V4/2-1/2
- RF of loop [15:1,17:1]:
V4 depends on loops [15:2,16:1]
- RF of loop [15:2,16:1]:
V depends on loops [15:1,17:1]
- RF of loop [16:1]:
V+V4+V5-1 depends on loops [15:2]


### Specialization of cost equations main/2
* CE 13 is refined into CE [24]
* CE 14 is refined into CE [25,26,27,28,29,30]
* CE 15 is refined into CE [31]


### Cost equations --> "Loop" of main/2
* CEs [29] --> Loop 20
* CEs [30] --> Loop 21
* CEs [24] --> Loop 22
* CEs [25,26,27,28,31] --> Loop 23

### Ranking functions of CR main(V,Out)

#### Partial ranking functions of CR main(V,Out)


### Specialization of cost equations start/3
* CE 2 is refined into CE [32,33]
* CE 3 is refined into CE [34,35,36]
* CE 4 is refined into CE [37,38,39,40]


### Cost equations --> "Loop" of start/3
* CEs [32,33,34,35,36,37,38,39,40] --> Loop 24

### Ranking functions of CR start(V,V4,V5)

#### Partial ranking functions of CR start(V,V4,V5)


Computing Bounds
=====================================

#### Cost of chains of fun(V,Out):
* Chain [14]: 0
with precondition: [Out=0,V>=0]

* Chain [13]: 1
with precondition: [V=Out,V>=1]

* Chain [multiple([12],[[14],[13]])]: 1*it(12)+1*it([13])+0
Such that:it([13]) =< V/2+1/2
aux(1) =< V
it(12) =< aux(1)
it([13]) =< aux(1)

with precondition: [Out>=1,V>=Out]


#### Cost of chains of fun1(V,V4,V5,Out):
* Chain [19]: 0
with precondition: [Out=0,V>=0,V4>=0,V5>=0]

* Chain [18]: 1
with precondition: [V+V4+V5=Out,V>=1,V4>=1,V5>=0]

* Chain [multiple([15,16,17],[[19],[18]])]: 1*it(15)+2*it(16)+1*it([18])+0
Such that:it([19]) =< V/2+V4/2+1
it([18]) =< V/4+V4/4+1/2
aux(212) =< V/2+V4/2
it(15) =< aux(212)
it(16) =< aux(212)
it([18]) =< aux(212)
it(16) =< it([19])* (1/2)+aux(212)

with precondition: [V>=1,V4>=1,V5>=0,Out>=0,V+V4+V5>=Out+1]


#### Cost of chains of main(V,Out):
* Chain [23]: 2*s(5)+6*s(6)+3
Such that:aux(215) =< V
aux(216) =< V/2
s(5) =< aux(216)
s(6) =< aux(215)
s(5) =< aux(215)

with precondition: [Out=0,V>=0]

* Chain [22]: 1
with precondition: [V=Out,V>=1]

* Chain [21]: 1*s(17)+3*s(18)+1*s(23)+1*s(25)+2*s(26)+3
Such that:s(24) =< V/2
s(23) =< V/4+1/4
aux(217) =< V
aux(218) =< V/2+1/2
s(18) =< aux(217)
s(17) =< aux(218)
s(25) =< s(24)
s(26) =< s(24)
s(23) =< s(24)
s(26) =< aux(218)* (1/2)+s(24)
s(17) =< aux(217)

with precondition: [V>=3,Out>=0,V>=Out+2]

* Chain [20]: 4*s(28)+4
Such that:aux(219) =< V
s(28) =< aux(219)

with precondition: [Out>=2,V>=Out+1]


#### Cost of chains of start(V,V4,V5):
* Chain [24]: 2*s(34)+14*s(35)+1*s(37)+1*s(39)+2*s(40)+2*s(43)+1*s(46)+1*s(51)+2*s(52)+4
Such that:s(38) =< V/2+V4/2
s(36) =< V/2+V4/2+1
s(46) =< V/4+1/4
s(37) =< V/4+V4/4+1/2
aux(220) =< V
aux(221) =< V/2
aux(222) =< V/2+1/2
s(34) =< aux(222)
s(35) =< aux(220)
s(34) =< aux(220)
s(43) =< aux(221)
s(43) =< aux(220)
s(51) =< aux(221)
s(52) =< aux(221)
s(46) =< aux(221)
s(52) =< aux(222)* (1/2)+aux(221)
s(39) =< s(38)
s(40) =< s(38)
s(37) =< s(38)
s(40) =< s(36)* (1/2)+s(38)

with precondition: [V>=0]


Closed-form bounds of start(V,V4,V5):
-------------------------------------
* Chain [24] with precondition: [V>=0]
- Upper bound: V/4+1/4+ (14*V+4+nat(V/4+V4/4+1/2)+nat(V/2+V4/2)*3+ (V+1))+5/2*V
- Complexity: n

### Maximum cost of start(V,V4,V5): V/4+1/4+ (14*V+4+nat(V/4+V4/4+1/2)+nat(V/2+V4/2)*3+ (V+1))+5/2*V
Asymptotic class: n
* Total analysis performed in 1425 ms.

(10) BOUNDS(1, n^1)